テクニカルレポート | GRACEセンター

ISSN 1884-0760

先端ソフト

ア工学に関するＧｒａce

国際

ンポ

ム

形式手法の産業応用ワーク

ョップ

WIA

M

: Workshop on Industrial Applications of

ormal Methods

予稿集

年

月

5 日

国立情報学研究所

はじめに

ソフト

ェア

社会

様々

製品やサービス

可欠

い

現在

ソフト

ェア

具合

起因す

シス

ム障害

時

し

社会

広範囲

つ深刻

影響を

え

います

こうした背

ソフト

ェア

信頼性向

へ

要求

さ

求

つつあ

ます

一方

海外

おい

数学的基盤

基

い

論理的

検証し

ソフト

ェア

を開発す

形式手法

つい

研究開発

長年

わた

実施さ

お

実問題へ

適用

本格的

始ま

います

日本

おい

開発現場へ

普及

始ま

い

ま

いえ

い状況

あ

ます

一部

開発現場

おい

適用

試

人材育成

取

組

始

います

本ワークショップ

形式手法

関す

研究開発

適用実践

人材育成

取

組

い

国内

研究者や技術者

一堂

会し

相互

情報交流や連携

機会

場を提供す

こ

を目的

し

います

今回

ワークショップ

形式手法

適用実践や人材育成を先駆的

取

組ま

い

有識者をゲスト

迎え

各活動

現状や今後

構想

つい

語

いた

ます

また

形式手法

実践

教育

係

具体事例

つい

専門家

紹

いた

く

形式

手法

教育

つい

パネル

スカッションを開催し

企業

おけ

形式手法

教育

現

状

課題

つい

議論をいたします

事前

参加

録者数

当初

予想を大幅

超え

100 名近く

録

あ

ました

形式手

法へ

関心

期待

高ま

い

こ

証

いえます

こ

機運をさ

盛

た

来年以降

ワークショップを開催す

予定

す

実行委員長：

粂野文洋

三菱総合研究所/国立情報学研究所

実行委員：來間啓伸

日立製作所/国立情報学研究所

、石川冬樹

国立情報学研究所

、田口研

形式手法の産業応用ワークショップ

2010

プロ

ラム

日時、場所：

年

月

5 日

国立情報学研究所

Session 1 (10:20- 11:50) 形式手法の展望

IPA/SEC

おけ

形式手法

関す

活動状況

課題

山本

修一郎

名

屋大学

情報連携統括本部

情報戦略室

教授

シス

ム検証研究センター

七年間

木

佳樹

産業技術総合研究所

シス

ム検証研究センター

形式手法

知識体系

FMBoK (Formal Methods Body of Knowledge)

構築

向け

田口研治

国立情報学研究所

GRACE

センター

Session 2 (14:20-15.50) 形式手法の実践

教育

ル検査知識体系

MCBOK2008

つい

西原秀明

産業技術総合研究所

組込

シス

ム技術連携研究体

IC

カ ー

セ キ ュ

開 発

お け

形 式 手 法

SPIN

適 用

Smartcard security

development using formal method tool SPIN

市原尚久

株

NTT

ータ

技術開発本部

SI

アーキ

クチャ開発センタ

ソフト

ェア開発

おけ

形式手法導入

関す

課題

解決アプローチ

石黒

正揮

(

株

)

菱総合研究所

情報技術研究センター

情報セキュ

研究

ループ

Session 3 (16:10-17:40) パネル

形式手法教育の現状と課題

企業内

形式手法教育を実践さ

い

方々や研修セ

ー

教育プロ

ラム等

社会

人を対象

した形式手法教育を実践さ

い

方々をパネラ

し

お招

し

各々

形式

手法教育

現状

つい

紹

いた

く

形式手法

開発現場

普及す

た

課題

つい

人材育成

観点

議論し

いた

ます

パネラ：小川清

名

屋市工業研究所

劉少英

法政大

青木利

Ａ

Ｓ

IPA/SEC

における形式手法に関する活動状況と課題

山本修一郎

ア ストラクト

IPA/SEC ，2007年 高信頼性シス ム技術 関す 調査検討会を発足さ ，こ ま 3年 わた 形式手法 産業界 活用 つい 産学官 議論を け た．本稿 形式手法 関す こ ま 活動状況を紹 す 今後 課題 つい 述 ．

Current status and future issues on Formal Method

activities of IPA SEC

Shuichiro Yamamoto

Abstract

IPA/SEC established an investigation group on the dependable system development technology in 2007. We have continuously discussed how to promote industrial application of Formal Method these 3 years in collaboration with members from Japanese industry, academia and SEC. In this article, I will introduce an overview of the activity and future issues to deploy Formal Method into Japanese industries.

1.

はじめに

2.

活動状況

高 信 頼 性 シ ス ム 技 術 調 査 検 討 会(DSTWG,

Dependable System Technology Working Group) IPAソ フト ェア ン ニア ン センター SEC 活動 ループ 一つ し 2007 年 発足した．こ

DSTWG 社会 浸透し 重要インフラ た情 報シス ム 引 起こすシス ム障害 社会的 大

影響を え た ，重要インフラシス ムを高信頼 化す た 技術を調査す た 2007年度 海外 び 国内 おけ 形式手法 導入状況を調査した．

2.1 体制とイ ント

2007年度 産7名，学5名，官6名 委員 参加 し 調査検討会を7回開催した．また，高信頼性シス ム開発手法フ ーラムを開催す ，高信 頼ソフト ェア構築技術 関す 動向調査報告書 を 公開した．

2008年度 産13名，学5名，官5名 委員 参加 し ，6回 高信頼性シス ム技術WGを開催した． また，日中高信頼性シス ム検討会 いうこ 中国

形式手法 研究者 意見交換した．また JAXA

IPA-SEC共催 ，第７回WOCS-Workshop Of Critical

Softwareを実施した． こ 結果，米国 び 欧州 形式手法 産業応

用を積極的 支援す た ，多数 研究機関やユー 企業 参加す 多く 国家プロ ェクトを進 い こ 明 た．こ た ，DSTWG

2008年 2009年 け ， 国 情報シス ム開発 形式手法を導入す た う 課題

あ ，そ を う し 解決し いく つい 議論を し た．こ う 議論を受け

2009年 DSTWGを発展さ こ ，形式手法 導入プロセス実証評価WG 発足す こ た．

2009年度 し 6回 高信頼性シス ム技術

WG を産16名，学7名，官8名 委員 開催し た．当初7名 参加 あ た産 委員 倍増し い こ 産側 期待 大 いこ 分 ．ま た3回 プロ ェクトチーム会議を組織し 形式手法 導入プロセス 実証 向けた準備検討を実施した． さ 高信頼シス ム開発技術 動向 つい 書 籍化を予定し い ．また，ソフト ェア ャパン

2010 ，ソフト ェア開発 パラ イム チェン

in イン IPA/SEC おけ 新しい取組 一つ し 形式手法 取 組 を紹 し い ． 以 DSTWG おけ 活動状況 主 調査結果

をま 紹 す ．次い 高信頼性シス ム技術 し 形式手法 産業応用 つい 課題認識 つい 述

．最後 形式手法 導入プロセス 実証 必要性 ，そ 進 方 つい 提言す ．

2.2 主 調査結果

†名古屋大学 情報連携統括本部 情報戦略室

†Information and Communication Planning Office, Headquarter of Information and Communication Services at Nagoya University

を表1 示す[1]．黒 示した 海外事例，赤 示した 国内事例 あ ．こ 表 多様 形式手 法 多方面 導入さ い こ ，そ 導入形態 一様 く多様 あ いうこ 分 ．

表１ 主 形式手法 導入事例 V Z v en t S S V

航空 テスト 設計， テスト

宇 探査衛星仕様 要 求 ， 設計

タミン グ

設 計 チップフー ム

仕様

設 計 ， テスト テ ス ト 設 計

JUAS 調査[2] ，シス ム規模 増大す ，開発予算 超過し品質 十分 ．た え 500人月以 プロ ェクト 50％以 予 算超過し約40％ 品質 十分 さ い ．こ 対し 100人月 満 プロ ェクト ，品質 十分

20％以 ，予算超過 10％程度 さ ．こ 結 果 示唆す こ ，大規模シス ム 分解 必要性 あ ．シス ムを分解す た アーキ クチャ 設計 重要 ．

原子力 設計

鉄道 仕様， 設計， 実装 状態設計

船舶 設計， テスト

公共 設計， 実装 医療 設計仕様記述

社内システム S 仕様 ベント セキュリテ 状態設計検証 運用設 設計

S ーネルテスト ード

携帯電話 プラットフーム設計 電力

組込機器 仕様

3.

課題

3.1 大規模化の影響

3.2 重要インフラ障害の原因

経済産業省 報告書[3] ，重要インフラ情報 シス ム障害 原因 ，開発21％，保守39％，運用

40％ い ．つま ，ソフト ェア開発時 をいく 削減し 重要インフラ障害 80％ く い いうこ あ ．した ソフト ェ ア開発時 運用 保守を考慮す こ 必要 ． す わち運用時や保守時 運用者や保守者 ソ フト ェア う 扱わ を考慮した仕様や 設計 求 ．

3.3 ｨ ンダビリティ

JIS Z 8115 ア イラビ 性能及びこ 影響を え 要因，す わち信頼性性能，保全性性 能及び保全支援能力を記述す た 用い 包括 的 用語 し ン ビ 定義さ い ．また，ア イラビ ， 要求さ た外部資源 用意さ た 仮定した ，アイ ム え た 条件 え た時点，また 期間中，要求機能を実

行 状態 あ 能力 し 定義さ い ．し た ，外部資源 ソフト ェア 対し 要 求さ 機能を実現す 性質 し ン ビ

を記述す こ 求 ．

4.

形式手法の導入プロセス

4.1 必要性

DSTWG こ ま 議論 明 たこ 次 う あ ．実際 ソフト ェア開発 形式手 法を導入す た ，現場 導入す た 実践的 プロセスを構築す 必要 あ ，こ 導入プロセス ，形式手法を導入し う す 対象プロ ェクト 置 た状況，つま 開発プロセス，担当者 スキル， 開発環境，プロ ェクト ー 意識 依存す ． 優 た形式手法やそ 自動化ツール た そ を現場 す 導入す いい いうこ

い．形式手法 長所 あ 限界 あ ，そ を う 個々 開発現場 プロセス 調整 調和さ いく いうこ 導入プロセス 込 た 意味合い 理解し い ．

高信頼性シス ム技術WG 2007年 発足当時 ，形式手法を産業界 導入す た ，技術面， 普及面，教育面 取 組 必要 あ ，そ 次

う 考え いた．

技術面 ，高信頼性開発技術フ ームワーク 策 定 開発ライフサイクル 対す 統合的開発手法 構 築 必要 ．普及面 ，実証研究 基 く成 事例蓄積 知識 体系化，国内研究機関 連携，国 際連携 取 組 必要 ．教育面 ，教材開 発 スキル認定 つい 検討 必要 ．

今回，形式手法 導入プロセス実証評価WG 形式手法 教育普及WG 発足した ，実証評価 教育普及 両輪 相補的 活動し いくこ 大

考え た あ ，こ 方針 当初 変わ い い．

4.2 導入プロセスの構成要素

前述したこ ，形式手法 導入プロセス 次 う 方法を具体的 明 す 必要 あ ． ソフト ェアをコンポーネント 分解し 仕様を記 述す 方法

運用環境や保守環境 ソフト ェア 外部 う 相互作用をす を記述す 方法

仕様 満たす 性質を記述す 方法 形式的 仕様を記述す 方法

仕様 性質を満たすこ を数学的 保証 こ 要求 ル，アーキ クチャ記述言語，形式手法 作 成プロセスを記述

仕様をコー 実現す 追跡性を確認 こ

実施組織 記 方法を開発プロセス 統合す こ

要求 ル，アーキ クチャ記述言語，形式手法を 用いた開発組織，適用組織 を記述

こ 目 うち 従来 形式手法 く知 い ． 大規模化す ソフト ェア 対し アーキ クチャ記述 親和性 高い形式手法を 確立す た 必要 あ ． 重要インフラ障害を 防 た 必要 あ ． 仕様 コー 一貫性を 保証す た 必要 ． 形式手法を実際 開 発プロセス 組込 た 必要 ．た え ，次 う 早期 スト駆動型V ル[4] し 開発 プロセスを確立す 必要 あ ．

取 組

要求 ル，アーキ クチャ記述言語，形式手法を 記述，適用，教育す た プロ ェクト管理面 具体的 取 組 を記述

こ 共通パターン 記述を ン ニア ン ース 呼ぶ． ン ニア ン ース 各プロ ェクト 置 た状況 ，形式手法 導入 当た う 課題 あ ，そ を う 解決した を記録す た ，具体的 あ 容易 理解 ．し し，一般化さ い い ，同

う 状況 け 使え い いう問題 あ ． また，一般的 手法を具体的 現場 状況 合わ カスタ イ す こ 非常 困難 問題 あ ．

要求

モデル

受入れ 試験

単体 試験

結合 試験

システム 試験

設計

ニメーシ ョンテスト

仕様

テスト項目生成

検証

検証

コード

証明 モデル検査

証明 テスト管理 テストシナリ

モデル検査

静的解析 動的解析

具体的 導入パターン 蓄積 そ 一般化 つい 研究を期待したい．

5.

まとめ

図１ 早期 スト駆動型V ル

本稿 ，IPA/SEC おけ 形式手法 関す 取 組 つい 述 た．また産業界 期待さ 形式 手法 導入プロセス 実証的 取 組 を進

課題 ，そ た 必要 導入プロセス 共通 的 パターン言語 し ン ニア ン ース 構 成を提案した．

4.3 エン ニ リン ケース

調査結果 示した う ，形式手法 導入 多様 分 急速 大しつつあ ．こ た 前述した導入 プロセスを適用対象シス ム 異 方法 記録 した ，多様 導入事例 蓄積 た し ， 滑 活用 困難 こ 予想さ ．こ た 次 う 形式手法を ， う 導入した

いう判断根 を記述す た 共通パターンを提案 し い ．

参考文献

1)高信頼ソフト ェア構築技術 関す 動向調査報 告書, http://sec.ipa.go.jp/reports/20080606.html 情勢変化

2)JUAS, 企業IT動向調査2007 要求 ル，アーキ クチャ記述言語，形式手法を

採用す 至 た開発 技術 情勢を記述

3)経済産業省，重要インフラ情報シス ム信頼性研究 会 報告書，2009, IPA

IT変容 期待

4)ROBERT M. HIERONS, et.al., Using Formal Specifications to Support Testing, ACM Computing Surveys, Vol. 41, No. 2, pp. 9-76, 2009

要求 ル，アーキ クチャ記述言語，形式手法 対象 したITシス ム変容へ 期待を記述

技術課題

要求 ル，アーキ クチャ記述言語，形式手法 達成し う したシス ム高信頼化へ 貢献 解決し た技術課題を記述

記述内容

システム検証研究センターの七年間

†

産業技術総合研究所

シス

ム検証研究センター長

木

佳樹

ア ストラクト

産業技術総合研究所 産総研 シス ム検証研究センター CVS 前身シス ム検証研究ラ ボ(LVS) 設置さ た 2003年4月 した 一年後 シス ム検証研究センター 改組し 以後 年間 研究センター し シス ム検証 関す 研究活動 技術移転活動を行 ま い ました 産総研 各研究センター 研究部門 長 年 仕事 内容 つい 理事 長 契約 を交わし そ 内容を 方針声明(policy statement) し 公 す こ

お ます ここ そ 中 主 目を拾い CVS 七年間 わた 活動を え たい 存 ます

1.

目標

2.

数理的技法

CVS活動 目標 数理的技法 いう研究対象 つい 明し おこ う 思います 近年 うやく 形式技法 形式手法

formal methods 開発現場 本格的 考慮さ う います い う シス ム 仕様 を機械処理可能 形式言語 記述す 完全 full 形式技法 け く 背 数理科学的 ルを持 ちつつ 仕様 記述自体 英語や日本語 書 記述 機械処理を必 し 可能 し い いう半 形式技法 semi-formal methods あ い ル指向 アプローチ model based approach あ ます 々 数理的技法 いう言葉を形式技法 ル指向ア プローチを包含す し 用い いますそこ 数理的技法 情報シス ム設計 関す 唯一 科学技 術 あ い い し う 逆 いう 情報シ ス ム設計 科学技術 あ そ 何

意味 数学を使う し う 数理的技法 呼 す 形式技法 いう言葉 何 特定 技 術 あ う 印象を え 事実 昨今 そ

う 誤解 広ま い う 感 す 実 そう あ ま

シス ム検証 数理的技法 情報処理シス ム開発 おけ 生産性お び信頼性 向 有効 あ こ を産業界 得し 数理的技 法を普通 検証法 す こ

す たくいう シス ム検証 数理的技法 技術移転を根本 目標 した す 研究所 し 当然 こ し 実用化研究 応用研究 や基礎研究 わた 研究活動 CVS 行 ま した し し CVS 全体 し 技術移転を通 し 産業界 一般社会 相互 作用す 活動を行う いうこ を こ 目標を掲 こ 言し た す

CVSを組織す あた 情報シス ムそ 関す 科学技術分 研究 技術開発 教育 立ち遅 い 観測 あ たこ を申し お たい 思います 研究センター発足 後 ０ ０ 年 日本経済団体連合会 意見書 産学官連携 高度 情報通信人材 育成強化 向け 出 さ 文部科学省 先導的ITス シャ スト育成プロ ラム 開始さ こ 立ち遅 社会的 広 く認知さ 至 ました ０08年 国立情報学 研究所 先端ソフト ェア工学･国際研究センター 設置さ います し し CVS 発足した時 情 報シス ム トラ ル 2010年 今日ほ 顕在化し いま した ソフト ェアトラ ル 起因す 携帯電話 回 大 くクロー アップさ ま ま 情報シス ムトラ ル 珍しい現象 し 扱わ た時代 した CVS 設置 時代を若 先取

した時宜 合 た た 自負し お ます

さ ここ 科学技術 うこう 々す 情報シス ム開発 おい 科学技術 呼 ほ

客観的事実 推論 積 重 伝え 技術体系 殆 い す 大規模 情報 シス ム 構築法 し 単 ルール 集積 し 先輩 後輩 見 う見ま 伝え 職人芸的

いく あ け い し う そ 結果 技術 伝 口伝 し おこ え 技術 者 急増 必要 現実 対応 い い う 思 わ ます

組込 シス ムや業務シス ムを す 情報 シス ム 開発現場 大規模シス ム全体を見通 すこ 困難 あ た 深刻 問題 多数発生し います こ 周知 お す こ 状況 1970 年代 いわ たsoftware crisis 本質的 同 す こ 問題 一朝一 解決す 思わ ま 数理科学を用い 職人芸 し く 科学技術 し 情報シス ム 開発技術を確立す こ

こ 本質的問題 立ち向 おう いう 々 立場 す

3.

科学研究とフィールドワーク

CVS シス ム検証 数理的技法を産業界 移転 す こ を目標 し 組織さ ました こ 分 研究 進 い い 科学研究 誰 行わ け

ま 数理的技法 ま ま こ 研 究 必要 分 あ まし いわ 枯 た分 十分 研究 さ つくした い た分 あ ま

一方 技術移転 優秀 研究者 携わ 大 い 望ましいこ す 研究者 意欲を た 環境を提供す た 技術移転 けを行 う組織

す わけ い ま そこ CVS 科学研究 技術移転を両方行 うこ を目指しました いわ waterfall式 考え 研究活動を 科 学研究 技術移転 間 分い い 活動 必要

す 科学研究 成果 実用化さ し そ 数十年 普通 す CVS設置期間 年間 間 技術移転ま 辿 着く 可能 す そ

科学研究 従事す 技術移転 無縁 い け い し う ？

科学研究 従事す 同時 技術移転 携わ こ し う 々 考えました こ 一つ 挑戦 した し し大学 既 似たこ 起こ います 大学 第一線 研究者 あ 教授 学生 学術を 移転 し います

ここ く考え 大学 研究 対象を そ まま学生 教え 限 ま カ キュラム を作 学部 学生 初歩 進 知識へ 順序立 学術を伝授す こ います こ 同 う 科学研究 対象 別 技術移転 対象を考え そ を順序 移転し いくこ す

い い 考えました つま わ わ

自 科学研究 対象をそ まま技術移転す こ こ わ い

こ した す 自分 研究対象 限 自分

研究分 周辺 研究成果 あ そ 技術を 移転す こ 適当 あ そ 技術 移転を行 うこ しました 々 自分 研究分 周辺 こ を 勉強し く知 い わけ し こ 研 究者 つ強 あ す

考え こ 当然 話 す 科学研究 科 学 世界 おけ 価値観 した 行 わ す そ 価値観 産業界や一般社会 価値観 同

限 ま 従 科学研究 結果を移転 う 技術 仕 そ た 特別 仕 事 必要 すこ CVS設立前後 産総研草創期 当時 川弘之理事長を中心 し 行 わ た 本格 研究 議論 お まし 川氏 第2種 基 礎研究 いう考え 主張さ たこ あ ました い い 世界 そこ 固有 価値観を持つ い う考え 民族学や大乗仏教 影響さ い

し ま 川氏 第2種 基礎研究 明 民族学者 Lévi-Strauss bricoleur 便利屋 日曜大工 考えを引用し お た 興味深いこ

す

こ う 技術移転 た 技術 移転先 世界 価値観を く知 す そ こ 自身

また 研究 近い活動 す 技術 移転先 世界を わ わ フ ール 考え こ 活動こそフ ール ワーク 呼ぶ さわしい し う 図

ここ 民族学 用語を借用す こ ました

科学研究 け 技術移転 け 大変 両方 や 可能 い 疑問 あ ました し し 大学 起こ い こ を見 こ す 肯定的 答え 出ました 産総研 学生 い

い 代わ 技術者を対象 した技術 移 転をす こ 可能 い い し う 大学 教育 関す 仕事を く educational

duty い います そこ いくつ 大学 講 演

industrial duty instead of educational duty

い た 教授連 喝采 若手研究者 ーイン を得たこ あ ます

あ CVS 科学研究 フ ール ワークを 分業 行 う く 各研究員 両方 携 わ こ を求 う した こ つ 意図 あ ました 一つ 最新 研究成果あ い 成果そ

技術移転 活動 中 新た 科学研究 対象を見 出す可能性を求 ました つま

科学研究 フ ール ワーク 相互作用 を求 た す 研究成果を産業や社会 適用す こ くいわ 逆 作用 あま 強調さ ま

こ こ つい 筆者 1990年代初頭 ン ラ大学滞在中 聴いた Robin Milner教授 lab

lunch お け 談 話 大 く 影 響 し い ま す dti

(department of trade and industry)を訪 た機会 実用 化 議論 し し 産業界 価値観 科学 価値 観 優先さ こ 暗黙 うち 仮定さ 逆 考え こ いう話をし た い う そ 内容 した 産業界 価値観 学界 価値 観 確 違う す し し ち 絶対 的 優先さ いうわけ あ ま 対等 価値観 つ並 い 考えた う いうわけ す 簡単 話 す 蒙を開 思い した す

各研究員 科学研究 フ ール ワーク 両方 携 わ う いう当初 考え し し 実務的理 由 簡単 崩 しまいました プロ ェクト費用 研究員 人件費を出し い 場合 あ そ 場 合 当然 プロ ェクト 専念す こ 求

す そこ そ う 場合 例外 し ました そ 場合 例え フ ール ワーク プロ ェクト 携わ い 研究員 対し 科学 研究をおこ うこ を け援助す こ しま した

両方 携わ 当た 具体的 う す 指針を え こ ま した し し 両者へ 労力配分

四分 原則

つま フ ール ワーク 四分 科学研究 分 く い 労力配分 や ほしい いう原則を作 ま した こ い い 応 あ ました 産総研 本 地つく 有名 四 蝦蟇 ち わけ

い す 英語 こ を講演した 4:6 書い た そ 約分し 2:3 す う いう意見 出 び く したこ あ ます 四分

いう言葉 語呂 英語 消え しまうわけ わ わ そ こ を 明す 羽目 ました フ ール ワーク 四分 労力し 割 い 少 す い いう管理側 意見 あ ました し し 労力 ： 成果 ７： 8: く い

す そ く い 科学研究 け け

い労力 大 い いうこ わ え い 残念 した ： ： ７ う し 測 いう生真面目 質問 対し そ う く 科学研究 割く労力をち 多 し く いう ッセー

いう う 明をした す

4.

コ

ュニケーション

コ ュニ ーションを重視す 方針声明 中 謳いました 研究活動 おい 同僚研究者 議論

大 役割を果たします 正確 コ ュニ ーショ ン た 書 い し う 考 えを交換し自分 考えをさ 進 いくた 会話 コ ュニ ーション 便利 す 研究

関す 会話 研究センター内 日常的 行 わ 当た 前 聞こえ し ま 実際 各研究者 個室 閉 こ しま 全く会話 い研究所 あちこち あ ます 一人 研究 進 研究所 要 い し ま 会話 研究を進 う 研究集団を作 こ を 々 望 ましたそ た 研究室 配置を工夫した 一人 研究員 複数 プロ ェクト 参加す こ を 奨励した しました

5.

共通知識基盤

情報シス ム検証や開発 数理的技法 いう分 わ 国 殆 講座 い そ 研究活動 必要 数理論理学 抽象代数学 プロ ラ ン 言語

また た知識 わ 国 大学 あま 教え いま そ 結果 CVS 論理学 数学 ソフト ェア工学 異 背 知識を つ研究者

集ま こ ました 背 違う研究者 会話 コ ュニ ーション 研究を進 考えを表現す 基盤 し 共通 必要

す そ た

z 数学的構造 複雑 概念を定式化す 有用 圏論

z 論理 計算 記述あ い 仕様プロ ラム 証明 記述 有効 構成的型理論

z プロ ラ ン 言語Haskell

つを共通知識基盤 し こ 枠組を使 考えを交換す こ を奨励し ました し し 結果を こ 部分的 し うまくい い い う す

構成的型理論 考え 急速 研究員 広 ました し し 圏論 CVS設置当初 いく 広ま た

七年目 現在 研究員 間 殆 使わ いま こ 研究センター 研究活動 当初想 定した 大幅 フ ール ワーク 寄 しま たた 圏論 有効性 明 う 複雑 数学的議論 あま 必要 く たこ 原因 あ

思わ ます 科学研究を強化す こ

圏論 有効性 また明 う 見 います

Haskell あま 浸透し いま こ 理由 つ 考え ます 一つ Agda言語 Haskellへ コン パイラ しま た Agda言語 分改良 加え 書 やすく た 函数型言語 し し 依存型ま 使え Agda言語を使う う たこ つま 当初 予想 し Haskell 要 しま たこ す 一方 実行時 高い性 能 求 場合 JavaやC++ 用い こ

たこ う一つ 原因 し あ ます こ う 具体的 掲 た知識基盤 研究員 ン ー 間 広 た あ 広 た あ ます 議論 土 枠組を共有し う い う試 研究組織 し 今後 常 け いく

考え います

6.

班とチーム

研究センター 全体 し 目標達成 た 働 け ま そ た い い 仕事を手 分けし 行 う す 一般 企画 計画 実行 後始 段階 一ま ま 仕事 手分 けす や 方 通 考え ます つ 分け方 仕事を いくつ 小さ 一ま ま 仕 事 わけ そ を手分けす こ す お お

小さ 一ま ま 仕事 そ ル 再び企画 計画 実行 後始 段階を持ちます う一つ

一ま ま 仕事を 企画 け 実行 け 後始 け 段階別 分け や 方 す 後者 極端 場合 Chaplin Modern times 風 さ た う 流 作業 ここま い しまう 作業 携わ

自身 仕事へ や いを感 く いこ く言わ お す

研究員 支援要員 含 た各 ン ー や いを

感 仕事を進 た け前者

や 方 仕事を手分けし 流 作業 陥 い う し 各 ン ー や いを感 仕事を

場所 したい 考えました そ た 一ま ま 仕事 つま プロ ェクト 一つ 班を

作 そ 見え 形 しました そうし 各 ン ー そ 立場や能力 応 企画 計 画 実行 後始 段階を全部経験し や い を感 仕事をし ほしい 期待しました

班を作 たお 誰 仕事 従事し い 明 ました ン ー 見 自分 仕事 関わ い を明確 す こ

ました こ ち いう い い こ を裁断し いく父性原理 や 方

包 こ う す 性原理 進 方を ち わ 国 理解さ くいこ た し ま

また や い う い 何をした 給料をく を さ ほしい まあ ここま 直接 言う 現 ま した 要す

そういう風 考え い い 組織管理 難しさを痛感さ たこ あ ます

産総研 導入さ た短期評価 た 班 制度 仕事を明確 し おくこ 評価者 被評価者 好都合 こ した お 班 う プロ ェクト指向 組織 筆者 産総研設立前 所属し いた電子技術総合研究所 最 後 何年間 既 ラボ いう名前 導入さ いた

そ 考えを借用し た す 各班 班長を設け ー を明確 しました し し 班長 班員 比 人間的 偉い いう く ー し 役割を負う け いうこ を強調しました 一般 研究センター ン ー 複数 班 所属す す あ 班 班長 班員 た関係 別 班 逆転し 班員 班長 関係

いうこ あちこち 起こ ました し し 々 そ こ を特 問題 し いま こ 点 つい 産総研中央 管理側 心配す 意見を いた いたこ あ ます 仕事を進 問題 を感 たこ あ ま

研究センター内部 組織 し 当初 仕事別 つく 班を作 け すす う した す す

ン ー別 組織 必要 感 ました 中 長期的 キャ ア 関す 世話 つま 進路相談や細 日常業務 関す 管理 また 途中 産総研 本格的 導入さ た勤務管理 を行 うた 各 ン ーを階層的 所属さ 別 組織を設け

属す いう形 組織を管理す こ ました 班 研究チーム う 通 組織を作 管理す

や 方 ト ックス管理 呼 い 既 い い 組織 行 わ い こ を 後 当時人 事担当 理事を務 お た小林直人氏 教示 いた ました

こ 班 研究チーム 管理 大体 こ う まく機能した 感 います 一年 短期評価 うまく ッチしたし 誰 仕事 従事し い

新た 加入した ン ー す わ う い う 思います

7.

企業との共同研究

産総研 改組後四年目 CVS 設置さ た す そ ン ー 科学研究 研究経歴を持つ

産総研改組前 企業 共同研究 経験 を持つ 皆無 した そ く ち

いう 産業 関係し 活動す こ 嫌悪す 傾 向 あ たこ 否 ま し し フ ール ワ ーク いう考え 企業 共同研究を開始した

こ こ こ 大変面 く や いを感 進 こ た う 思います 先輩 そ ほ 産業 協業を強調し 若手 研究員 納 得す ？ 心配をいた いたこ あ ます 若手研究員 連中 ほう 産業 協業を面 た 場合 あ ます 尤 徹底的 産業 協業を嫌う い たわけ あ ま フ ール ワ ークを面 い 感 最後ま 残 い い う け こ し ま 別 先輩 研究者

あま 実用化研究をさ いほう いい いう あ そ を始 た 皆 面 く や

く 基礎研究 携わ い く いう話をし く ました 若 怪し あ ます 実用化研究 面 い い う こ 今 々 くわ う 思います

数理的技法 情報シス ム検証 手法 す 手法 研究を企業 共同 行う いう つま こ そ 企業 おい そこ 開発現場 手法 適用を実験す いうこ つ ます 々 フ ー ル ワーク 称し 行 た企業 共同研究 す そ う した こ う 共同研究を 行う あた

縁側 奥座敷へ

を し LVS/CVS活動七年間を おし い くつ 蓄積しました

こ つい

木 佳樹 高井利憲： フ ー ル ソッ フ ール ワーク 情報処理 第49巻第

5号 第9-15頁 ま あ ます

8.

連携検証施設

さつき

と組込みソ

フト産業推進会議

2007年秋 首都圏鉄遈改 シス ム トラ ル を契機 経済産業省 組 込 シス ム 信頼性 向 技術 た 産学官連携施設をCVS 産総 研 おけ 活動を支援し 充す こ し 検証向 け 設計さ たクラスタコン ュータ 関西センター 設置さ こ ました 産総研内 こ た 連携検証施設 さつ CFV を設置しました こ 相次い 関経連 組 込 ソフト産業推進会 議 推進会議 活動を 年間 予定 開始し つ 活動 相互 作用し 大規模 連携活動を生 出 しつつあ ます クラスタコン ュータ を使 た 検証サービス 組込 適塾 名付けた研修コース提 供 つを した事業 開始さ お 推進会 議 設置 2010年春 終了した後 関経連側 後 組織をつく 活動を す こ います さつ 学術利用 行 お jopshop

scheduling problem 解決問題解決 成果 得 います

9.

研修コース開発と組込み適塾

手法 適用実験を企業 技術者 行う ま 彼 技術者たち 手法を身 つけ 必要 あ こ フ ール ワークを開始した初期 うち 明確

ました そこ 適用実験 用い 技術を技術者 伝え た 研修コースを本格的 開発す こ し ました こ ま ル検査 コース 対話型定理 証明 コース を試行コース し 無料 提供し 延 名以 技術者 対し 研修を提供しました こ をカ キュラム化す こ 開始し お

CVS教程 シ ー し ル検査初級 級 教科書を プト ア社 刊行し います 以 CVS 研修活動 加え 2008年 推進会議 関西センター 共催 組込 適塾を開催し

います 約30名 受講者 対し 3ヶ月 わた

い こ ま 研修コース開発 活動 す 研修 技術移転 中 し 位置 け 活動 す 今後 最 重要 活動 一つ し け いく

考え お ます

10.

法定計量のソフト

認証

産総研 重要 任務 一つ National Measurement

Institute し わ 国 法定計 検定型式 認 管 理 あた こ あ 計 標準総合センター そ 任 あた います 最近 計 器 殆 皆計算機 制御 お そ 中 ソフト ェアを う 型式 認す 国際的 問題 います 産 総研設立 直前 たまたま田中充氏 計測標準分 担当研究コー ネータ 当時計測標準研究部門副部 門長 関西センターを訪 た そ 話をさ たこ け CVS ソフト ェア認証 関 し お手伝いす こ ました 当時 非自動

組込 ソフト ェア認証 関す ーロッパ 規格 あ け した 現在 一般 計測器 関し

ソフト ェア認証を導入す た イ ライン

OIML 公式文書D31 し 定 お 前後し タクシー ータ 非自動 既 ソフト ェア認証 開始さ います こ 活動 た

CVS 名 研究員 計測標準研究部門 移籍 し 任 あた います こ 当時計測標準研究部 門長 あ た小 氏 現副理事長 ソフト ェア 認証を重要案件 し 積極的 支持さ た結果 あ

思 お ます

法定計 ソフト ェア認証 関係した を け 機能安全や ン ビ ほ 分

ソフト ェア認証 仕事 開始し います あ 紹 す 利用者指向 ン ビ 研究 こ 方向 仕事 す こ 仕事 計算機シス

ム 社会シス ムへ留 を向け けを え く た う 思います

11.

今後―検証を不要にするために

2010年3月 CVS 年間 設置期限 終了し た後 殆 ン ー CFV(Collaborative Facilities

for Verification―連携検証施設) おい 活動を けま す

こ ま シス ム 検証 焦点を当 活動し ました 実 そ そ 検証 いう作業 行わ い 済 理想 し う 誤 い情報シス ムし い う 開発 方法 あ C by C―

correctness by construction いう言葉 使わ た し

います こ う 方法 あ そ 越した こ あ ま 従 今後 シス ム 検証

シス ム 開発全般 わた 技術 研究 対象 を 大し いく し う そ ソフト ェア工 学あ い ソフト ェア科学 いわ い 近 い すけ 々 取 い 数理科学 基 くアプローチ 対象をソフト ェア 限定す 必要

あ ま 情報を処理す シス ム あ ー ェア まわ いし 企業や法人 う 社会 組織を対象 す こ ます 最近進展しつつあ 法 工学 いわ 分 そ 一部 す こ う 分 を 呼ぶ 算譜科学 記述 科学

形式手法

知識体系

FMBoK (Formal Methods

Body of Knowledge)

構築に向けて

口研治

†

国立情報学研究所

GRACE

コンタヴ

形式手法 Formal Methods 情報クケゾヘ 信頼性ン安全性を保証 る開発技術 注目され ある 、形式手法 多く 異 る特徴を持 言語ン表記法、検証技術 あり、それらを使いこ

実践的 知識 十分 確立され いる 言え い状態 ある 、そ 教育ィモ ゥュメヘ 標準化 知識体系 確立され い い状態 ある 本論文 い 、形式手法 知 識体系 FMBoK (Formal Methods Body of Knowledge) 構築 試 い 、そ 構想 目標、体制

い 述 る ある

Towards Building a Body of Knowledge on Formal

Methods (FMBoK)

Kenji Taguchi

National Institute of Informatics, Grace Center

Formal Methods have been gaining attention as a development method for assuring reliability and safety of information systems. However formal methods comprise of a wide variety of formal languages/notations and verification methods and their best practices have not been established yet. In addition to this, the curricula have not been standardized due to lack of a body of knowledge. This paper will give an overview on an initiative to build a body of knowledge on formal methods (FMBoK) and touches on its vision including its goal and working team.-

1.

じめに

現在 情報社会 い 、情報クケゾヘ 安全性

社会全体 大 影響を及 要因 、非常 大

ゞ゠゜ダを占 いる 電気ン電子関連機器 国

際安全規格 あるISO IEC 61508 [1]，コゥュモゾ゛ 保 証 関 る 国 際 標 準 Common Criteria (ISO/IEC

15408) [2] い ，形式手法 Formal Methods

利用 推奨や，利用 義務化等，クケゾヘ 信頼性ン

安全性を検証 る技術 形式手法 関心 高

り ある さら ，産業界 い いく 本格

的 活用 報告され いる ，形式手法 多

く 異 る特徴を持 言語ン表記法，検証技術 あり，

これらを使いこ 実践的 知識 十

分 確立され いる いえ い 現状 ある 本

論文 い ，こ よう 状況を打破 る 方

策 ，形式手法 Formal Methods ける知識

体系構築 要性を論 るこ を目的 いる

ソネダゞゟ゚工学 い SWEBOK(Software

Engineering Body of Knowledge) [3] や SE 2004 [5]

知られ いる これらを用い 形式手法 教育を行え

充分 ある， いう考え方 ある ，現在，

形式手法 非常 多岐 渡り研究開発 進ん り，

そ ん SWEBOK い 網羅され い

い 現状 ある

形式手法 い 知識体系 最初 論 られ

J. Oliveira [8] い ある これ ， FME (Formal

Methods Europe) ける教育を担当 るサノエャ

ヴハFME-SoE (Subgroup on Education) い ，実施

され 教育調査を元 ，知識 分類を行 あ

る 残念 ら，体系的 り け いる

あ 々 ペ タ ャ 検 査 限 知 識 体 系

MCBOK 構築を実施 り[9,12,13]，そ 体系

を基 ， FMBoK 構築を考え いる

本論文 い ， 章 い 工学ン科学分

け る 知 識 体 系 い 概 観 ， 章 い

FMBoK 構想 い ，そ 目標，体制 い 述

るこ 示 そ ，最後 ， 章 い 結論

を述 る

2.

BoK

と

BoK ある工学ン科学分 ける知識を表現

る 要 概念，技術 構 的 集 り ，それ 対

る共通理解を意味 る BoK 技術的用語 理

工学ン科学分 い 知識体系 BoK (Body of

Knowledge) 構築され いるソネダゞゟ゚工学

分 い ，既 述 IEEE Computer Society

ACM 共同 構築 SWEBOK や SE 2004

知られ いる ハログゟェダ管理分 い

PMBOK (Project Management BOK) [4] Project

Management Institute (PMI) より構築され いる こ

れら よう 広い領域を網羅 る BOK 以外 非

常 小さ 技術領域を対象 る を存在 る

PSP (Personal Software Process) 関 る BOK [6] そ

例 ある

BoK 知識を木構 より表現 る ，木構

深さ 対 一定 制限を るこ ，理解度

可 性を保持 いる BoK 主目的 知識 分類を

行うこ ある ，そ 詳細 明や関連文献

い 文書 イ゜チ より与えられる 例え

，SWEBOK 対 ，実際 流布 いる

イ゜チ ある

BoK 目的 教育 けるィモゥュメヘ 標準化

同時 ，そ 分 ける実務者 対 る資格認定

大 役割 ある 例え ， PMI 5 資格認 定を行 いる こ 二 目的 ， BoK 構築

い 利害 衝突を生 さ る場合 ある 現在，ソ

ネダゞゟ゚工学 ける ゜ニク゚ゾ゛ノ，

SWEBOK，SE2004，Certified Software Development

Professional (CSDP) を改訂 る動 ある そこ

い ，大学教育 ける知識体系 SWEBOK, SE

2004 ，資格認定 CSDP ける知識体系をブ

ヴグさ る いう ある

3.

FMBoK

本章 い ， FMBoK 目指 目標，知識体系，

゜ニク゚ゾ゛ノ 体制 構想 関 述

る

3.1 目標

FMBok 役割 ，通常 BoK 二

役割，教育ィモゥュメヘ 標準化 資格認定 両

方 役割を目指 ある 特 ，゚ハロヴチ

，当初 ら資格認定を 視 る ある こ

理 ，2章 述 ソネダゞゟ゚工学 け

る 3 ゜ニク゚ゾ゛ノ い 現在，ブヴグ る努

力 行われ いる ，大学 ける教育ィモゥュメ

ヘ 標準化 ソネダゞゟ゚開発者 資格認定

ィモゥュメヘを 々 開発 ，そ

整合性を取る努力 後 必要 こ 起因 る

ら ある

知識体系 ，形式手法全体を網羅的 ィトヴ

る ある ペタャ検査分 関 る知識体系

MCBOK (Model Checking Body of Knowledge) [9,12,13]

チメネダ版 い 既 発表を行 り，そ

際 知見を FMBoK 構築 活 こ を考え いる

3.2 知識体系

知識体系を構築 る ，主 知識領域

Knowledge Area, KA を何 る を決定 る必要

ある 例え ， SWEBOK い ，主 ，開発

ハロコケ 沿 知識領域を設定 いる 形式手法

開発ハロコケ全体 い 用いられ いる， いう

より 要求 様 ら始 り，設計，構築 construction

け 点的 利用され いる

こ よう 考え 基 ，知識体系 ，開発

ハロコケ 沿 構築 る 無く，各技術ン理論

分 構築 る方法を取るこ を構想中 ある

り，ペタャ検査 知識体系，形式 様記述 知識体

系，定理証明 知識体系 い 知識領域を設定 ，

開発ハロコケ 特徴 い ，各知識領域内 取

り扱う いう方法 ある こ よう 方法を採用 る

理 ， 記 分 専門家 分化

いる， いう現状 ある ，形式 様記述言語

対 るペタャ検査や定理証明 要素技術

存在 る ，そ よう 場合 ，各知識体系間

相互参照を行うこ より， 複を避けるこ を考

え いる

3.3 活動状況と今後 体制

これ 著者 形式手法 知識体系 構築 向け ，

様々 活動を行 2008年 FMET (Formal

Methods Education and Training) 国際ワヴェクョッハ

[10] を M. Hinchey (Lero, U. Limerick)， J. Davies, J.

Gibbons (U. Oxford) ら 組織 本ワヴェクョッハ

論文 後 ACM SIGCSE ら刊行され [11] さ ら 2009年 い ，FME 主催 TFM (Teaching

Formal Methods) 国際会議 い FMBoK い

ドネャ討議を るこ ，FMBoK ゚゜タ゚ 深化，

協力者を募 ドネャ チゟ゚ M. Hinchey

ドネモケダ 著者，P. Larsen, J. Oliveira, R. Johnson 今後 FMET, TFM を中心 本活動を組織 るこ

を計画 いる

FMBoK 当初 ら国際化を目指 構築 る を

目指 り，そ 体 FME-SoE 共 行動

るこ 合意され いる さら ，作業ベントヴ

，産学官 ける研究者，実際 利用 いる

開発者 両方を含 ，トメンケ 取れ チヴヘ構 を

主ベントヴ ある，西原 産業技術総合研究所クケゾ ヘ検証コンタヴ，青木 JAIST，篠崎 関電，早水 ベャコドワヴゲ，粂 MRI，NII，石川 NII

を中心 ，より広くベントヴを募集 る予定 ある

4.

終わりに

本論文 い ，形式手法 知識体系 FMBoK を

よう 構築 る い 構想を述 本知識

体系 特徴 ，当初 ら大学 形式手法教育 ，

開発者 資格認定 両者を行うこ を想定 構築

行われる， いう特徴 あり，組織作り い そ

考えを考慮 いる

よう 工学分 い BoK 存在 る い 過言 い ，必 BoK 技術，学 術教育 解決方法 無い 例え ， D. Notkin ら [7]

い SWEBOK 対 る批 を いる 本゜ニ

ク゚ゾ゛ノ これら 様々 先見者 より得られ 知

見を反省曩料 ，構築を行うこ を目指 いる

参考文献

1)IEC61598: Functional safety of

electrical/electronic/programmable electronic safety-related systems. Bureau Central de la Commission Electrotechnique International, 2000.

2)ISO/IEC 15408: Information technology – Security techniques –Evaluation criteria for IT security – Part1, Part2 and Part3, 2005.

3)A. Abran, J. W. Moore, P. Bourque, and R. Dupuis: Guide to the Software Engineering Body of Knowledge, 2004 version SWEBOK, IEEE, 2004.

4)Project Management Institute: Guide to the Project Management Body of Knowledge (PMBOK Guide), Forth Edition, PMI, 2008.

5)The Joint Task Force on Computing Curricula: Software Engineering 2004, IEEE and ACM, 2004.

6)M. Pomeroy-Huff, R. Cannon, T. A. Chick, J. Mullaney, and W. Nichols: The Personal Software Process (PSP) Body of Knowledge, Version 2.0, CMU/SEI-2009-SR-018, 2009. 7)D. Notkin, M. Gorlick and M. Shaw: An Assessment of the Software Engineering Body of Knowledge. A Report to the ACM Council, 2000.

8)J. N. Oliveira: A Survey of Formal Methods Courses in European Higher Education. In Teaching Formal Methods (TFM) ’04 Conference Proceedings, pp 235-248. LNCS 3295, Springer, 2004.

9)青木, 粂 , 木 , 篠崎, 高木, 高曪, 口, 中原,

西原, 早水, 本位 , 渡邊: ペタャ検査 教育ハロエメ ヘ構築 向け ”, 算譜科学研究 報, 独 産業技術

総合研究所,クケゾヘ検証コンタヴ, AIST-PS-2008-012.

2008.

10) J. Davies, J. Gibbons, M. Hinchey, K. Taguchi (editors): Proceedings of the first international workshop on Formal Methods Education and Training,

GRACE-TR-2008-03, GRACE Center, National Institute of Informatics, October 2008

11) J. Davies, J. Gibbons, M. Hinchey, K. Taguchi: A preface on Special section on Formal Methods Education and Training, ACM SIGCSE Bulletin inroads, vol. 41, issue2, June, pp14-16, 2009.

12) H. Nishihara, K. Shinozaki, K. Hayamizu, T. Aoki, K. Taguchi, F. Kumeno: Model Checking Education for Software Engineers in Japan, ACM SIGCSE Bulletin inroads, vol. 41, issue 2, June, pp45-50 2009. 13) 西原, 青木, 粂 , 篠崎, 口, 早水:

MCBOK2008:ソネダゞゟ゚開発 ペタャ検査

モデル検査知識体系

MCBOK2008

について

西原秀明

モデル検査教育の質の向上と技術の普及を目指し，大学・産業界に属する組織と共同で教育体系の 基礎付けを進めている．著者らが行ってきた教育活動の概要と結果について述べた後，モデル検査分 野の知識を体系づけてまとめたMCBOK 2008についてポイントや利用法を説明する．

On Model Checking Body Of Knowledge 2008

Hideaki NISHIHARA

Activities on modelchecking training for engineers are discussed. The Activities are in col-laboration with NII, JAIST, KEPCO, MPS, and CVS/AIST. Training courses managed by authors are reviewd and evaluated. Next, a foundamental document of model checking called Model Checking Body Of Knowledge 2008 is introduced.

1.

は じ め に

本稿の内容は国立情報学研究所(NII)，北陸先端科学

技術大学院大学(JAIST)，関西電力(KEPCO)，メル

コ・パワー・システムズ(MPS)との共同研究4),11),12)

をもとにしている．

近年，情報処理システムの普遍化，複雑化によって，

システムに要求される信頼性はますます高くなってき

ており，形式手法が注目されている．特にモデル検査

は人間が見落としがちな想定外の振る舞いを全数探索

によって発見することができ，強く期待されている．

この数年では産業界一般における認知度も高まり，国

内でもシステム開発における本格的な導入が進み，多

方面の分野における適用事例や企業により開発され

たツール が発表されるなど注目されている．さらに，

モデル検査を科目として持つ大学のカリキュラムや人

材育成プログラムも増えてきているし，モデル検査を

特色としてあげるコンサルテーション企業も存在する．

著者らは産，学，官それぞれの立場から技術者向け

モデル検査の教育・普及を進めてきたが，更に普及を

推進することを目的に連携し，より一般的な見地から

活動している．

まず，お互いの研修活動やカリキュラムについて情

報を交換し，技術者向けモデル検査教育のあるべき

†産業技術総合研究所組込みシステム技術連携研究体

Collaborative Facilities for Verification, National In-stitute of Advanced Industrial Science and Technol-ogy(AIST)

姿を検討した4),12)．その結果は第2節，第3節で述

べる．

その検討を受けて，モデル検査技術の普及を推進す

るためには，統一的な基礎付けが必要だという認識に

至った．つまり，モデル検査に関する知識を体系化し，

新たなカリキュラムの開発や既存カリキュラムの比較

の際の基礎資料とすべきである．

関連する分野で，上記のように教育の基礎となるも

のとしてはソフトウェア工学の教育に関する

SWE-BOK1)

，SE20046), J0710) などがある．しかしその 中には，形式手法がトピック名として現れている程度

で，モデル検査とその知識については殆ど記載がない．

そこで，著者ら自身でモデル検査の知識を体系化し

た11)．その成果である知識体系を「ソフトウェア開発

のためのモデル検査知識体系(MCBOK 2008)」と呼

ぶことにする．

MCBOK 2008は「モデル検査のプロセス」，「モデ

ル検査の理論」，「モデル検査ツール」，「モデル検査の

適用対象」の四つの領域を持ち，モデル検査の知識が

存在する広い範囲から知識項目を収集して体系化して

いる．各領域は段階的に副領域に分割され，その中に

「有限オートマトン」「内部モデル/外部モデルの設計」

「NuSMV」といった知識項目が分類されている．

MCBOK 2008はモデル検査カリキュラムの基礎的

な資料として機能する．第5節で述べるように，著

者らがこれまで進めてきた教育活動のカリキュラムと

の対応づけを考えることで，カリキュラムの扱う内容

る際にも，到達目標に合った教育する知識の選択を支

援する．その他，技術認定の枠組み構築や，コンサル

テーションなど，モデル検査の関係する幅広い活動の

基礎資料として機能することを期待している．

2.

カリキュラムの比較

著者たちが行ってきた，技術者向けモデル検査研修

について述べる．トップエスイー(NII)，JAIST 組

込み大学院，MPSによる研修テキスト，CVS/AIST

研修コースそれぞれのカリキュラムを比較し，受講者

からの評価を紹介する4)(但し 2007年時のデータで

ある)．

開催形態は以下の通り．

NII スーパーアーキテクト育成プロジェクト「トッ

プエスイー」の中でモデル検査に関係する科目7

科目を持つ．各科目につき，週一回の講義12回．

受講者対象はSW 科学専攻の修士修了程度の知

識を持つ社会人．

JAIST 組込み大学院科目「ソフトウェア検証手法」

(週一回の講義15回)，日科技連セミナー「ソフ

トウェアモデル検査入門」(3日間集中)．社会人

対象．

MPS 社内セミナー基礎編(12時間)・応用編(40時

間)・実践編(80–160時間)．受講者対象は社内の プログラマ，設計者．

AIST モデル検査研修コース初級編(4日間集中)・

中級編(3日間集中)・上級編(3日間集中)．初級

編受講者対象は，プログラミングの経験を持つ学

生・開発者．

表 1は各カリキュラムの共通点と相違点について

まとめたものである．各カリキュラムにおいて，ツー

ル，論理体系，システムの性質，抽象化，検証プロセ

ス，基礎理論，と理論から実践までバランスよく項目

が扱われている．モデル検査は従来の開発手法・検証

手法と異なり，理論的基盤である数学や論理について

一定の知識が必要であること，受講者の背景知識や経

験が多様であることから，カリキュラムで扱うべきこ

とは少なくない．実際，研修期間をもっと長く確保し

たかったという意見も出ている．また，各カリキュラ

ムでは実践・現場への適用を念頭においており，検査

ツールの機能，操作や検証プロセスについても扱って

いる．教材で扱われる例題や演習も，近年モデル検査

の適用領域として注目されている組込みシステム関連

から選ばれていることが多い．

一方，カリキュラム間の相違点も少なくない．AIST

のカリキュラムでは理論に属する内容を多く扱ってい

表1 モデル検査教育内容の比較

Table 1 Common/Peculiar topics in courses

共通項目 非共通項目 ツール

·Spin

·SMV

並行システム 論理体系

·LTL

·CTL

システムの性質

·安全性

·活性

·公平性 抽象化

·抽象化写像

·構造の保存定理

·データ抽象化

·述語抽象化 検証プロセス 基礎理論

·有限/Buchiオートマトン

·CTLモデル検査

AIST:

·LTLとCTLの比較

·遷移系の合成

·Kripke構造への変換

·空語判定問題

·有界モデル検査

TopSE:

·時間オートマトン

·LTSA MPS

·実システムの検証

表2 アンケート結果

Table 2 Questionnaire Results

アンケートの設問に対して，好評価(平均点以上)の回答数を集計

受講者数 理解度 有用さ 実施可能性

AIST (初級) 75 59(79%) 70 (93%) N/A

AIST (中級) 24 7 (29%) 24 (100%) 18 (75%)

TOPSE (基礎) 36 22 (61%) N/A 26 (72%)

TOPSE (応用) 7 5 (71%) N/A 5 (71%)

JAIST 61 58 (95%) 54 (89%) 43 (70%)

MPS 13 10 (77%) N/A 10 (77%)

合計 216

161/216 (74%) 148/160 (93%) 102/141 (72%)

るほか，TopSEでは複数のツールを用いてモデル検

査ツール一般の知識を伝えようとしている．JAISTの

コースではシステムプログラムを題材にしたモデルを

百余り準備し，実際の適用の様子を想起させている．

また，MPSの研修では，社内教育の利点を活かし，実

際の開発対象を題材にして開発業務の中でモデル検査

の経験を積ませるという手法をとっている．

モデル検査という技術は多様な分野と関連を持って

いて，個別の対象領域・問題に合ったツールや知識の

選択が課題の一つになることを示している．新たにカ

リキュラムを策定する際にはその理念と到達目標を確

認した上で内容を決めていくことが必要である．

3.

評

価

それぞれのカリキュラムで研修終了後に受講者アン

受講者からの評価は良好であった(表2)．

内容の理解度，モデル検査の有用性と実施可能性そ

れぞれについて，各カリキュラムで肯定的な回答が多

かった．このことは受講者のモデル検査に対する期待

を示していると同時に，技術者向けモデル検査カリ

キュラムとして適切なものであったことを示している．

自由形式によるアンケート回答から以下のような意

見が得られた．

• 多くの受講者がモデル検査の分析力を評価してお

り，そのことは表の「有用性」に対する回答が非

常に良かったことにも現れている．特に並行動作

システム，非決定的に振る舞うシステムのように，

人力で検査できない対象に対する検査能力には驚

いており，学習への動機付けとして効果が高い．

• より実践的な知識についての要望が強い．具体的

なシステムのモデル化，検査式の作りかたや，従

来の開発プロセスにモデル検査プロセスをどのよ

うに当てはめるか，といった事柄に対しての質問

や要望が多かった．

• 論理記号や抽象概念に対する苦手意識が強い．ま

た理論を学ぶモチベーションは低い．

これらの意見は教材改善のポイントを示唆している．

実践的な知識への要望については，実際のところ個別

の適用領域や個別の開発手法に対してモデル検査の適

用方法を整理し教材を準備することは現実的でない．

しかし，典型的な成功事例を題材として扱うことで適

用の指針を伝えることは可能である．記号や概念につ

いては，その意義や具体例との関連を充分に示すこと

や，導入の工夫により改善できる．適切なモデル化，

適切な検査式の作成，抽象化など，モデル検査では理

論を効果的に用いて検査の質を高められる場合が少な

くない．具体例により意義と効果を示しつつ理論的知

識を伝えるなどの工夫が必要である．

4.

MCBOK

前節のカリキュラムに関する議論を受けて，モデル検

査の知識を体系づけてまとめた11)．これをMCBOK

2008と呼ぶ(本稿末尾に掲載)．

ある分野における知識を体系化してまとめたものを

知識体系(Body Of Knowledge)と呼び，BOKと略 記する．知識には用語・概念のような理論に属するも

のも含まれるし，実践の際にノウハウとして適用され

るようなものも含まれる．関連分野ではソフトウェア

工学知識体系SWEBOK1)，プロジェクトマネジメン

ト知識体系PMBOK5)やソフトウェア品質知識体系

SQuBOK13)などが発表されている．また「情報専門

学科カリキュラム標準J07」10)には領域ごとに定めら

れたBOKが同梱されている．

多くのBOKでは対象領域に関する知識を三段階か

ら五段階程度の樹形図の上に配置することで構造を可

視化している．BOKに求められるものは，本質的に

この樹形図だけであって，そこに現れる知識の解説や

参照文献などは「ガイド」として別に扱うことが多い．

4.1 モデル検査のプロセス(KA 1)

以下の節で MCBOK 2008の領域ごとに簡単な説

明を加える．

KA 1. ではモデル検査をソフトウェア開発に適用

する際の知識があげられている．

KA 1.1では目的と工程によってモデル検査の適用

に関する知識を整理している．一般にモデル検査は設

計検証の技法と言われているが，最近ではソースコー

ドの検査事例や開発ツールに統合されているものもあ

り多様化している．

KA 1.2「モデル検査の適用手順」にはモデル検査

を適用するというプロセス自体についての知識を整理

している．検査範囲の特定，モデルの抽象度決定，外

部環境の構築，モデル検査で検査できる性質，ツール

の実行などが含まれている．

モデル検査を開発に適用するに当たり，そのコスト

や実施体制は大きな問題となる．KA 1.3「モデル検

査のコスト」，KA 1.4「モデル検査の実施体制」で

それらの知識を整理している．

4.2 モデル検査の理論(KA 2)

KA 2は理論的基礎に関する知識を体系化した領域

である．

KA 2.1「計算モデル」にはモデルを記述するための

枠組みを整理した．多くのモデル検査ツールでは有限

オートマトン，またはそれに類する各種の構造を使っ

てモデルを記述する．個々の計算モデルについて，そ

れを基盤とする検査ツールがあり，ソフトウェア開発

における適用例があるものを選んで知識項目として採

用した．

KA 2.2「時相論理」には検査式を記述する論理体

系について整理した．現在モデル検査で使われている

論理体系はLTLとCTLを基にしている．それぞれ

の意味論と決定可能性，表現力をここで扱う．

KA 2.3「モデルの縮小手法」は状態爆発問題の回

避方法に関する知識を整理した．モデル化の対象の分

析によってモデル化の範囲を縮めることで縮小する方

法もあり，一旦モデル化したものを機械的に縮小する

方法もある．縮小の前後を比較し正当性を示す手段も

KA 2.4「モデル検査の原理」では，モデル上での

検査式の妥当性を検査するアルゴリズムの知識につい

て整理した．

4.3 モデル検査ツール(KA 3)

KA 3はモデル検査ツールに関する知識を体系化し

た領域である．ソフトウェア開発における適用例があ

り，動作原理についての文献が存在しているものを採

用した．

KA 3.1はモデル検査アルゴリズムを実行するツー

ルを整理した領域である．モデル検査ツールは個々に

基盤となる理論，入出力の形式，検査規模の限界，検

査できる性質が異なり，6個の領域に分かれている．

KA 3.2はモデル検査アルゴリズムを実行するもの

ではないが，検査作業を支援するツールを整理して

いる．

4.4 モデル検査の適用対象(KA 4)

「モデル検査の適用対象」は適用事例を分類したも

のである．モデル検査は理論的な適用範囲は広く，殆

ど全てのシステムを適用対象とすることができるが，

適用効果が高い分野とそうでない分野がある．また，

未だモデル検査が日常的に使われているとは言いがた

い現状にあって，適用例を整理してまとめておくこと

にはMCBOKの目的からも価値がある．

5.

MCBOK

の利用法

MCBOK 2008の目的はモデル検査における知識の

構造を可視化し，産業界(主にソフトウェア開発分野)

へのモデル検査の普及を推進することである．主目的

は教育の際の基礎資料であるが，他にも幾つかの利用

法が考えられる．

5.1 カリキュラムの基礎付け

第2節で述べたように，モデル検査を学ぶには様々

な背景と目標が考えられ，教育内容や教育の順序その

他も多彩なものが考えられる．現在，技術を身につけ

たい開発者も，開発プロセスへの適用方法を知りたい

管理者も，同じカリキュラムで学ばざるを得ないが，

実はそれぞれ目的を満足する教授内容は異なる．それ

ぞれの目的に応じてMCBOKの各知識領域から必要

な知識項目を選択し，カリキュラムを構成することで

効率のよい知識の習得が可能になる．

逆に既存のカリキュラムに対して，扱われる内容を

MCBOK 2008の各知識とを対応づけることによって

そのカリキュラムを評価できる．表3 は産総研のモ

デル検査初級のカリキュラム12)について，各項目の

MCBOK 2008 の対応する知識領域を表したもので

ある．このカリキュラムには「モデル検査のプロセス

表3 産総研モデル検査初級カリキュラムから

MCBOK 2008へのマッピング

Table 3 Mapping from AIST’s curriculum to MCBOK 2008

カリキュラム項目 対応する知識領域 モデル検査とは

状態,遷移,次の瞬間,非決定的/決定的 1.2(4),2.1(1)

安全性,活性 1.2(2)(6)

モデル検査の基礎

状態と遷移を定めて状態遷移系を書く 1.2(1)(4) 検査する性質:正しい性質/反例のある性質 1.2(2) 遷移系を目でみて検査 1.2(7) ツールによるモデル検査 1.2(5)(6)(7)(8) 検査式の記述

直列回路,並列回路, And/Orの導入 1.2(6)

Until operator 1.2(6)

並行システムと排他制御

並行システム/セマフォ/Critical Section 1.2(4)(5),

2.1(1), 4.2

検査:同時にCSに入らない 1.2(2) 検査:各プロセスともCSに入ることが可能 1.2(2) 公平性の問題 2.1(1)

LTL

パス,パス上の真偽 2.2(1)

様相記号 2.2(1)

意味論 2.2(1)

LTL式を書く演習 1.2(2)(6),2,2(1) ソースコード検査

簡単なCプログラムのモデル化 1.2(4)(5), 4.1 テスト技法とモデル検査の違い

-演習:自動販売機 1.2(4)(5)(6)

(7)(8), 4.1

(KA 1)」の知識が多く扱われており，モデル検査の

適用のしかたに興味を持つ学習者に適していることが

わかる．

5.2 保有する知識の可視化

個人や組織が，自身が持つ技術の程度を知るツール

としてもMCBOK 2008は有効に働く．モデル検査に

関して幾らかの知識を持つ技術者が，MCBOK 2008

に挙げられている個々の知識について，

• モ デ ル 検 査 の 適 用 時 に ，そ の 知 識 を 意 識 し て い

るか，

• その知識を自分なりに知識として整理して使って

いるか，

を確認することで，その技術者が保持する知識や適用

時に意識していることを明確にできる．同様に不足し

ている知識，その時点では必要でない知識も明確にな

り，将来の学習計画を立てる際にも有用である．

5.3 モデル検査の適用の指針

システム開発プロセスへのモデル検査導入を検討す

る際のツールとしてMCBOK 2008は機能する．開